\section{Determinize}
\label{App:DeterminizeAlgorithm}

We found the explanations of how to determinize NWAs that are given
in~\cite{DLT:AM2006,JACM:AM2009} to be confusing (and contradictory between
the two accounts), and so we reformulated it using relational
operations.

We use the following notation in the determinize algorithm: \\
\begin{quote}
\begin{tabular}{ll}
  $(Q, \Sigma, \delta, Q_0, Q_f)$\hspace{1em}
                                     & The components of the input automaton \texttt{nwa} \\
  $\delta_i|_\sigma$                 & The binary relation $\{(p,q) | (p, \sigma, q) \in\delta_i\}$ \\
  $\delta_c|_\sigma$                 & The binary relation $\{(p,q) | (p, \sigma, q) \in\delta_c\}$ \\
  $\delta_r|_\sigma$                 & The binary relation $\{(p,q) | \exists c. (p, c, \sigma, q) \in\delta_r\}$ \\
  $R \circ S$                        & Relational composition of the binary relations $R$ and $S$ \\
  $R^*$                              & Transitive closure of the binary relation $R$ \\
  $Q^{new}, \delta^{new}$            & Components of the determinized NWA \\
\end{tabular}
\end{quote}
We use the following auxiliary function to compute the target of
a return transition:
\begin{eqnarray*}
  \textrm{Merge}(R^{exit}, R^{call}, \delta) = \{(q, q') & |& \exists q_1, q_2.\,(q, q_1) \in R^{call} \\
                                                         &&  \phantom{\exists q_1, q_2.\,}\textrm{and}\ (q_1, q_2) \in R^{exit} \\
                                                         &&  \phantom{\exists q_1, q_2.\,}\textrm{and}\ (q_2, q_1, q') \in \delta\}
\end{eqnarray*}

Each state $R$ in the determinized automaton is a binary relation on states
in the original. In a standard determinized FA, a state $\{q_0, q_1,
\cdots, q_n\}$ means the automaton can be in state $q_0$ of the original FA, or in
state $q_1$ of the original, etc. For NWAs, a state $\{(p_0, q_0), (p_1,
q_1), \cdots, (p_n, q_n)\}$ means that the NWA is one of the states $\{q_0,
q_1, \cdots, q_n\}$, but the relation carries around extra meaning.

If a state in the determinized automaton contains a pair $(p,q)$, then this
means the input automaton can begin in the state $p$, immediately perform a call
transition, follow a path with balanced calls and returns, and finally arrive
in state $q$. In such a configuration, if the input automaton then reads a
return symbol, $q$ is the exit site and $p$ is the call predecessor. These
two pieces of information are exactly what the automaton needs to decide what
return transitions it can take. The call predecessor $p$ needs to be stored
explicitly because it is possible to arrive at the same state $q$ with
different call predecessors.

At the start of the run, and any time the automaton has not read any pending
calls, the first component of each pair in the current state will be some $q
\in Q_0$; this is because the initial states act as call predecessors in that
situation.

\newcommand{\WL}{\textit{WL}}

\newpage
\begin{algorithm}[H]
  \hrule
  \DontPrintSemicolon
  \SetAlgorithmName{Listing}{listing}{listing}
  \SetKw{Int}{int}
  \SetKw{Boolean}{bool}
  \SetKwBlock{DetDef}{determinize(NWA nwa)}{end}
  \SetKwFunction{Merge}{Merge}

  \DetDef{
    $Close$ = $(\delta_i |_\epsilon)^*$\;
    $R_0$ = $Q_0 \times Q_0 \circ Close$\;
    $Q^{new}$ = $\{R_0\}$\;
    Insert $R_0$ in \WL\;
    \While{$\WL \neq \varnothing$}{
      select and remove a relation $R$ from \WL\;
      \tcp{Note that $R$ is a state in $Q^{new}$}
      mark $R$\;
      \For{$\sigma\in\Sigma$}{
        \tcp{Compute internal transitions}
        $R^i$ = $R \circ \delta_i|_\sigma \circ Close$\;
        $Q^{new}$ = $Q^{new} \cup \{R^i\}$\;
        Insert $R \overset{\sigma}{\rightarrow} R^i$ into $\delta_i^{new}$\;
        \If{$R^i$ unmarked}{
          $WL$ = $WL \cup \{R^i\}$\;
        }
        \BlankLine
        \tcp{Compute call transitions}
        $R^c$ = $Close \circ \delta_c|_\sigma \circ Close$\;
        $Q^{new}$ = $Q^{new} \cup \{R^c\}$\;
        Insert $R \overset{\sigma}{\rightarrow} R^c$ into $\delta_c^{new}$\;
        \If{$R^c$ unmarked}{
          $WL$ = $WL \cup \{R^c\}$\;
        }
        \BlankLine
        \tcp{Compute return transitions where $R$ appears as the exit node}
        \For{$R^{call} \in Q^{new}$}{
          $R^r$ = $\Merge(R, R^{call}, \delta_r|_\sigma) \circ Close$\;
          $Q^{new}$ = $Q^{new} \cup \{R^r\}$\;
          Insert $(R, R^{call}, \sigma, R^r)$ into $\delta_r^{new}$\;
          \If{$R^r$ unmarked}{
            $WL$ = $WL \cup \{R^r\}$\;
          }
        }
        \BlankLine
        \tcp{Compute return transitions with $R$ as the call predecessor}
        \For{$R^{exit} \in Q^{new}$}{
          $R^r$ = $\Merge(R^{exit}, R, \delta_r|_\sigma) \circ Close$\;
          $Q^{new}$ = $Q^{new} \cup \{R^r\}$\;
          Insert $(R^{exit}, R, \sigma, R^r)$ into $\delta_r^{new}$\;
          \If{$R^r$ unmarked}{
            $WL$ = $WL \cup \{R^r\}$\;
          }
        }
      }
    }
    \tcp{end worklist while loop}
    $Q_f^{new}$ = $\{R \in Q^{new} |\ \textrm{there is}\ (p,q) \in R
                                      \ \textrm{with}\ q \in Q_f\}$\;
    \Return{$(Q^{new}, \Sigma, \delta^{new}, \{R_0\}, Q_f^{new})$}\;
  }
  \hrule
\end{algorithm}
